COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST T F ε Proposition
C00006 00003	axiom future:
C00010 00004	declare INDCONST Tm ε Thingconcept
C00011 ENDMK
C⊗;
declare INDCONST T F ε Proposition;
declare INDVAR Q Q0 Q1 Q2 Q3 Q4 ε Proposition;

DECLARE OPCONST And(Proposition,Proposition) = Proposition [L←655,R←650];
DECLARE OPCONST Or(Proposition,Proposition) = Proposition [L←635,R←640];
DECLARE OPCONST Implies(Proposition,Proposition) = Proposition [L←615,R←620];
DECLARE OPCONST Equiv(Proposition,Proposition) = Proposition [L←605,R←610];
DECLARE OPCONST Not(Proposition) = Proposition [R←675];

declare INDVAR X X0 X1 X2 X3 X4 ε Thingconcept;
declare INDVAR x x0 x1 x2 x3 x4 ε thing;
declare OPCONST Equal(Thingconcept,Thingconcept) = Proposition [L←685,R←690];
declare INDCONST world ε worlds;
declare INDVAR w w1 w2 w3 w4 ε worlds;

declare PREDCONST ttrue(Proposition) [R←600];
declare PREDCONST true(worlds,Proposition);
declare OPCONST Nec(Proposition) = Proposition [R←700];
declare PREDCONST nec(Proposition) [R←600];
declare PREDCONST prec(worlds,worlds) [inf];

declare OPCONST denot(worlds,Thingconcept) = thing;

declare INDCONST Mike Joe Pat ε Personconcept;
declare INDCONST mike joe pat ε person;
declare INDVAR P P1 P2 P3 P4 ε Personconcept;
declare INDVAR p p1 p2 p3 p4 ε person;

moregeneral Thingconcept ≥ {Personconcept};
moregeneral thing ≥ {person};

declare OPCONST Telephone(Personconcept) = Thingconcept[R←710];
declare OPCONST telephone(person) = thing [R←599];
axiom teldef:	∀P w.(denot(w,Telephone P) = telephone denot(w,P));;

declare OPCONST K(Personconcept,Proposition) = Proposition;
declare PREDCONST k(person,Proposition);

declare OPCONST Know(Personconcept,Thingconcept) = Proposition;
declare PREDCONST know(person,Thingconcept);

declare OPCONST Want(Personconcept,Proposition) = Proposition;
declare PREDCONST want(person,Proposition);

declare OPCONST Like(Personconcept,Personconcept) = Proposition;
declare PREDCONST like(person,Personconcept);

declare OPCONST Future(Proposition) = Proposition [R←695];
declare PREDCONST future(Proposition) [R←597];

declare INDVAR E E0 E1 E2 E3 E4 ε Eventconcept;
declare INDVAR A A0 A1 A2 A3 A4 ε Actionconcept;

declare OPCONST Cause(Eventconcept,Proposition) = Proposition;
declare OPCONST Do(Personconcept,Actionconcept) = Eventconcept;
declare OPCONST Occur(Eventconcept) = Proposition [R←695];
declare OPCONST Tell(Personconcept,Thingconcept) = Actionconcept;
axiom future:
	∀Q w.(true(w,Q) ⊃ true(w,Future Q))
	∀Q w.(true(w,Future Future Q) ⊃ true(w,Future Q))
	∀Q1 Q2 w.(true(w,Future Q1) ∧ nec Q2 ⊃ true(w,Q1 And Q2))
	∀w Q.(true(w,Future Q) ≡ ∃w1.(w prec w1 ∧ true(w1,Q)))
;;

axiom logic:
	∀Q1 Q2 w.(true(w,Q1 And Q2) ≡ true(w,Q1) ∧ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Or Q2) ≡ true(w,Q1) ∨ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Implies Q2) ≡ true(w,Q1) ⊃ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Equiv Q2) ≡ (true(w,Q1) ≡ true(w,Q2)))
	∀Q w.(true(w,Not Q) ≡ ¬true(w,Q))
;;

axiom tell:
	∀P1 P2 X w.(true(w,Know(P1,X)) 
⊃ true(w,Cause(Do(P1,Tell(P2,X)),Know(P2,X))))
	∀P1 P2 Q w.(true(w,K(P1,Q)) ⊃ true(w,Cause(Do(P1,Tell(P2,Q)),K(P2,Q))))
;;

axiom likewant:
	∀P1 P2 Q w.(true(w,Like(P1,P2)) ∧ true(w,K(P1,Want(P2,Q)))
⊃ true(w,Want(P1,Q)))
;;

axiom cause:
	∀E Q1 Q2 w.(true(w,Cause(E,Q1)) ∧ true(w,Cause(E,Q2))
⊃ true(w,Cause(E,Q1 And Q2)))
	∀E Q w.(true(w,Occur E) ∧ true(w,Cause(E,Q)) ⊃ true(w,Future Q))
;;

axiom wantdo:
	∀P Q A w.(true(w,Want(P,Q)) ∧ true(w,K(P,Occur Do(P,A) Implies Future Q))
⊃ true(w,Occur Do(P,A)))
;;

axiom nec:
	∀P Q.(∀w.true(w,Q) ⊃ ∀w.true(w,K(P,Q)))
;;

axiom introspection:
	∀P X w.(true(w,Know(P,X)) ⊃ true(w,K(P,Know(P,X))))
	∀P Q w.(true(w,K(P,Q)) ⊃ true(w,K(P,K(P,Q))))
	∀P X w.(true(w,Want(P,X)) ⊃ true(w,K(P,Want(P,X))))
	∀P1 P2 w.(true(w,Like(P1,P2)) ⊃ true(w,K(P1,Like(P1,P2))))
	∀P Q1 Q2 w.(true(w,K(P,Q1)) ∧ true(w,K(P,Q1 Implies Q2)) ⊃ true(w,K(P,Q2)))
;;
declare INDCONST Tm ε Thingconcept;
axiom problem1:
	true(world,Know(Pat,Tm))
	true(world,Want(Pat,Know(Joe,Tm)))
;;

axiom problem2:
	true(world,Want(Joe,Know(Joe,Tm)))
	true(world,K(Joe,Know(Pat,Tm)))
	true(world,K(Joe,Like(Pat,Joe)))
;;